k:, i, j:k. Bij(k; k; (i, j)) 

latex

Definitions	Bij(A; B; f), Inj(A; B; f), Surj(A; B; f), P & Q, P  Q, Prop, (i, j), x:A. B(x), {i..j}, x:A. B(x), t  T, , i=j, if b t else f fi, Unit, P  Q, , b, A, b, False
Lemmas	assert wf, not wf, bnot wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, eq int wf, ifthenelse wf, bool wf, nat wf, int seg wf, flip wf